Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		a__from(X)	→ cons(mark(X),from(s(X)))
2:		a__first(0,Z)	→ nil
3:		a__first(s(X),cons(Y,Z))	→ cons(mark(Y),first(X,Z))
4:		a__sel(0,cons(X,Z))	→ mark(X)
5:		a__sel(s(X),cons(Y,Z))	→ a__sel(mark(X),mark(Z))
6:		mark(from(X))	→ a__from(mark(X))
7:		mark(first(X1,X2))	→ a__first(mark(X1),mark(X2))
8:		mark(sel(X1,X2))	→ a__sel(mark(X1),mark(X2))
9:		mark(cons(X1,X2))	→ cons(mark(X1),X2)
10:		mark(s(X))	→ s(mark(X))
11:		mark(0)	→ 0
12:		mark(nil)	→ nil
13:		a__from(X)	→ from(X)
14:		a__first(X1,X2)	→ first(X1,X2)
15:		a__sel(X1,X2)	→ sel(X1,X2)

There are 16 dependency pairs:


16:		A__FROM(X)	→ MARK(X)
17:		A__FIRST(s(X),cons(Y,Z))	→ MARK(Y)
18:		A__SEL(0,cons(X,Z))	→ MARK(X)
19:		A__SEL(s(X),cons(Y,Z))	→ A__SEL(mark(X),mark(Z))
20:		A__SEL(s(X),cons(Y,Z))	→ MARK(X)
21:		A__SEL(s(X),cons(Y,Z))	→ MARK(Z)
22:		MARK(from(X))	→ A__FROM(mark(X))
23:		MARK(from(X))	→ MARK(X)
24:		MARK(first(X1,X2))	→ A__FIRST(mark(X1),mark(X2))
25:		MARK(first(X1,X2))	→ MARK(X1)
26:		MARK(first(X1,X2))	→ MARK(X2)
27:		MARK(sel(X1,X2))	→ A__SEL(mark(X1),mark(X2))
28:		MARK(sel(X1,X2))	→ MARK(X1)
29:		MARK(sel(X1,X2))	→ MARK(X2)
30:		MARK(cons(X1,X2))	→ MARK(X1)
31:		MARK(s(X))	→ MARK(X)

Consider the SCC {16-31}. The constraints could not be solved.

Tyrolean Termination Tool (36.36 seconds) --- May 4, 2006